A Formulae-as-Types Notion of Control